Make the alignment configurable by mkannwischer · Pull Request #1379 · pq-code-package/mldsa-native

mkannwischer · 2026-08-11T04:05:21Z

Add two experimental config options: MLD_CONFIG_ALIGN sets the alignment of large buffers and structures in bytes, MLD_CONFIG_ALIGN_ATTRIBUTE replaces the declarator prefix for compilers whose spelling mldsa-native does not know. MLD_DEFAULT_ALIGN, MLD_ALIGN and MLD_ALIGN_UP derive from them.

The x86_64 and AArch64 backends reject an alignment below what their load and store instructions require.

MLD_TOTAL_ALLOC_* is measured for the default alignment, so it is no longer defined once the alignment is customized, and the allocation test skips itself in that case.

Partially addresses Exposing MLD_ALIGN for allocators and customization #1346

Add two experimental config options: MLD_CONFIG_ALIGN sets the alignment of large buffers and structures in bytes, MLD_CONFIG_ALIGN_ATTRIBUTE replaces the declarator prefix for compilers whose spelling mldsa-native does not know. MLD_DEFAULT_ALIGN, MLD_ALIGN and MLD_ALIGN_UP derive from them. The x86_64 and AArch64 backends reject an alignment below what their load and store instructions require. MLD_TOTAL_ALLOC_* is measured for the default alignment, so it is no longer defined once the alignment is customized, and the allocation test skips itself in that case. - Partially addresses #1346 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

oqs-bot · 2026-08-11T05:58:48Z

CBMC Results (ML-DSA-65, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	31s	7s	+343%
`mld_attempt_signature_generation`	⚠️	138s	31s	+345%
`sign_keypair_internal`	⚠️	26s	3s	+767%
`sign_pk_from_sk`	⚠️	52s	5s	+940%
`sign_verify_internal`	⚠️	161s	71s	+127%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1338s	1482s	-9.7%
`sign_verify_internal`	⚠️	161s	71s	+127%
`mld_attempt_signature_generation`	⚠️	138s	31s	+345%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	138s	201s	-31%
`poly_pointwise_montgomery_c`	✅	65s	116s	-44%
`mld_invntt_layer`	✅	58s	108s	-46%
`sign_pk_from_sk`	⚠️	52s	5s	+940%
`polyvecl_chknorm`	✅	50s	43s	+16%
`compute_pack_t0_t1`	⚠️	31s	7s	+343%
`sign_keypair_internal`	⚠️	26s	3s	+767%
`fqmul`	✅	22s	40s	-45%
`mld_ntt_layer`	✅	21s	43s	-51%
`sig_unpack_hints`	✅	13s	1s	+1200%
`sign_signature_internal`	✅	12s	6s	+100%
`keccakf1600x4_permute_native`	✅	11s	22s	-50%
`mld_ntt_butterfly_block`	✅	11s	25s	-56%
`poly_ntt_c`	✅	11s	22s	-50%
`rej_uniform`	✅	11s	7s	+57%
`rej_uniform_c`	✅	10s	16s	-38%
`polyt0_unpack`	✅	9s	13s	-31%
`rej_uniform_native_x86_64`	✅	8s	-	new
`sign_keypair`	✅	8s	4s	+100%
`poly_uniform_eta_4x`	✅	7s	13s	-46%
`mld_check_pct`	✅	6s	12s	-50%
`mld_keccakf1600_permute_c`	✅	6s	7s	-14%
`poly_chknorm_c`	✅	6s	13s	-54%
`polyveck_decompose`	✅	6s	14s	-57%
`caddq`	✅	5s	2s	+150%
`keccak_absorb_once_x4`	✅	5s	10s	-50%
`pointwise_acc_native_x86_64`	✅	5s	5s	+0%
`pointwise_native_x86_64`	✅	5s	2s	+150%
`poly_invntt_tomont_c`	✅	5s	10s	-50%
`poly_permute_bitrev_to_custom_optional_native`	✅	5s	3s	+67%
`polyveck_caddq`	✅	5s	7s	-29%
`polyvecl_ntt`	✅	5s	7s	-29%
`sign_verify_pre_hash_shake256`	✅	5s	6s	-17%
`keccakf1600x4_xor_bytes_native`	✅	4s	2s	+100%
`make_hint`	✅	4s	3s	+33%
`mld_sample_s1_s2`	✅	4s	6s	-33%
`montgomery_reduce`	✅	4s	1s	+300%
`pack_sig_z`	✅	4s	1s	+300%
`pack_sk_s1`	✅	4s	3s	+33%
`poly_caddq_c`	✅	4s	5s	-20%
`poly_challenge`	✅	4s	5s	-20%
`poly_decompose_c`	✅	4s	8s	-50%
`poly_invntt_tomont_native`	✅	4s	5s	-20%
`poly_use_hint_native_x86_64`	✅	4s	-	new
`polyeta_pack`	✅	4s	1s	+300%
`polyeta_unpack`	✅	4s	4s	+0%
`polyt1_unpack`	✅	4s	3s	+33%
`polyvec_matrix_pointwise_montgomery_row`	✅	4s	8s	-50%
`polyveck_reduce`	✅	4s	6s	-33%
`reduce32`	✅	4s	2s	+100%
`shake256_squeeze`	✅	4s	4s	+0%
`sign_signature_extmu`	✅	4s	4s	+0%
`sign_signature_pre_hash_internal`	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	✅	4s	7s	-43%
`sign_verify_extmu`	✅	4s	2s	+100%
`yvec_get_poly`	✅	4s	3s	+33%
`intt_native_x86_64`	✅	3s	4s	-25%
`keccak_absorb`	✅	3s	3s	+0%
`keccak_f1600_x1_native_aarch64`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	2s	+50%
`keccakf1600x4_permute`	✅	3s	1s	+200%
`mld_compute_pack_z`	✅	3s	5s	-40%
`mld_ct_get_optblocker_u8`	✅	3s	4s	-25%
`mld_ct_sel_int32`	✅	3s	2s	+50%
`mld_prepare_domain_separation_prefix`	✅	3s	4s	-25%
`mld_sign_attempt`	✅	3s	-	new
`pack_sig_c`	✅	3s	3s	+0%
`pack_sig_h`	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	✅	3s	1s	+200%
`poly_chknorm`	✅	3s	3s	+0%
`poly_chknorm_native_x86_64`	✅	3s	4s	-25%
`poly_ntt_native`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	4s	-25%
`poly_reduce`	✅	3s	4s	-25%
`poly_shiftl`	✅	3s	3s	+0%
`poly_sub`	✅	3s	4s	-25%
`poly_uniform_eta`	✅	3s	5s	-40%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint_c`	✅	3s	2s	+50%
`polyvec_matrix_expand`	✅	3s	6s	-50%
`polyveck_invntt_tomont`	✅	3s	7s	-57%
`polyveck_ntt`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery_c`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	✅	3s	1s	+200%
`polyvecl_unpack_eta`	✅	3s	2s	+50%
`polyvecl_unpack_z`	✅	3s	1s	+200%
`polyz_unpack_17_native_aarch64`	✅	3s	2s	+50%
`polyz_unpack_c`	✅	3s	9s	-67%
`rej_eta`	✅	3s	5s	-40%
`rej_eta_native`	✅	3s	3s	+0%
`shake128_release`	✅	3s	2s	+50%
`shake128_squeeze`	✅	3s	3s	+0%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256_absorb`	✅	3s	4s	-25%
`shake256_init`	✅	3s	4s	-25%
`shake256x4_absorb_once`	✅	3s	2s	+50%
`sign_signature`	✅	3s	5s	-40%
`sign_verify_pre_hash_internal`	✅	3s	5s	-40%
`sk_s1hat_get_poly`	✅	3s	3s	+0%
`unpack_pk_t1`	✅	3s	2s	+50%
`unpack_sk_s1hat`	✅	3s	1s	+200%
`decompose`	✅	2s	4s	-50%
`fqscale`	✅	2s	3s	-33%
`intt_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccak_finalize`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_permute_native`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`mld_ct_abs_i32`	✅	2s	6s	-67%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_h`	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	2s	+0%
`mld_sample_s1_s2_serial`	✅	2s	3s	-33%
`mld_sign_finish`	✅	2s	-	new
`mld_value_barrier_i64`	✅	2s	2s	+0%
`mld_value_barrier_u32`	✅	2s	4s	-50%
`mld_value_barrier_u8`	✅	2s	1s	+100%
`ntt_native_aarch64`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	✅	2s	6s	-67%
`pointwise_native_aarch64`	✅	2s	3s	-33%
`poly_add`	✅	2s	7s	-71%
`poly_caddq_native`	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	✅	2s	2s	+0%
`poly_chknorm_native`	✅	2s	4s	-50%
`poly_decompose_32_native_aarch64`	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_native`	✅	2s	5s	-60%
`poly_invntt_tomont`	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	2s	+0%
`poly_power2round`	✅	2s	7s	-71%
`poly_uniform`	✅	2s	2s	+0%
`poly_uniform_4x`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	3s	-33%
`poly_use_hint_native`	✅	2s	7s	-71%
`polyt1_pack`	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	✅	2s	3s	-33%
`polyveck_pack_eta`	✅	2s	3s	-33%
`polyvecl_pack_eta`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	✅	2s	4s	-50%
`polyw1_pack`	✅	2s	3s	-33%
`polyw1_pack_32`	✅	2s	2s	+0%
`polyw1_pack_88`	✅	2s	3s	-33%
`polyz_unpack`	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`power2round`	✅	2s	2s	+0%
`rej_uniform_eta_native_aarch64`	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native`	✅	2s	4s	-50%
`sign_verify`	✅	2s	6s	-67%
`sk_t0hat_get_poly`	✅	2s	1s	+100%
`sys_check_capability`	✅	2s	1s	+100%
`unpack_sk_s2hat`	✅	2s	3s	-33%
`unpack_sk_t0hat`	✅	2s	4s	-50%
`use_hint`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_init`	✅	1s	4s	-75%
`keccakf1600_permute`	✅	1s	4s	-75%
`keccakf1600_xor_bytes`	✅	1s	4s	-75%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	✅	1s	4s	-75%
`mld_ct_cmask_neg_i32`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	✅	1s	1s	+0%
`mld_ct_get_optblocker_u32`	✅	1s	3s	-67%
`mld_ct_memcmp`	✅	1s	4s	-75%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	1s	2s	-50%
`mld_polymat_expand_entry`	✅	1s	3s	-67%
`mld_sign_resume`	✅	1s	-	new
`ntt_native_x86_64`	✅	1s	5s	-80%
`poly_caddq`	✅	1s	3s	-67%
`poly_chknorm_native_aarch64`	✅	1s	2s	-50%
`poly_decompose`	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	✅	1s	2s	-50%
`poly_ntt`	✅	1s	2s	-50%
`poly_uniform_gamma1_4x`	✅	1s	3s	-67%
`poly_use_hint_native_aarch64`	✅	1s	4s	-75%
`polyt0_pack`	✅	1s	5s	-80%
`polyveck_chknorm`	✅	1s	36s	-97%
`polyveck_pack_w1`	✅	1s	4s	-75%
`polyveck_unpack_eta`	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery`	✅	1s	3s	-67%
`polyz_pack`	✅	1s	3s	-67%
`polyz_unpack_native`	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	✅	1s	3s	-67%
`rej_eta_c`	✅	1s	4s	-75%
`rej_uniform_native_aarch64`	✅	1s	5s	-80%
`shake128_absorb`	✅	1s	2s	-50%
`shake128_finalize`	✅	1s	2s	-50%
`shake128_init`	✅	1s	6s	-83%
`shake128x4_absorb_once`	✅	1s	2s	-50%
`shake256`	✅	1s	2s	-50%
`shake256_finalize`	✅	1s	1s	+0%
`shake256_release`	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sk_s2hat_get_poly`	✅	1s	1s	+0%
`unpack_sk`	✅	1s	3s	-67%
`yvec_init`	✅	1s	5s	-80%

oqs-bot · 2026-08-11T05:58:48Z

CBMC Results (ML-DSA-44, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	29s	12s	+142%
`mld_attempt_signature_generation`	⚠️	142s	19s	+647%
`sign_keypair_internal`	⚠️	21s	4s	+425%
`sign_pk_from_sk`	⚠️	39s	5s	+680%
`sign_verify_internal`	⚠️	154s	49s	+214%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1213s	1364s	-11.1%
`sign_verify_internal`	⚠️	154s	49s	+214%
`mld_attempt_signature_generation`	⚠️	142s	19s	+647%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	99s	149s	-34%
`poly_pointwise_montgomery_c`	✅	65s	112s	-42%
`mld_invntt_layer`	✅	54s	105s	-49%
`sign_pk_from_sk`	⚠️	39s	5s	+680%
`compute_pack_t0_t1`	⚠️	29s	12s	+142%
`mld_ntt_layer`	✅	24s	41s	-41%
`fqmul`	✅	22s	39s	-44%
`sign_keypair_internal`	⚠️	21s	4s	+425%
`keccakf1600x4_permute_native`	✅	13s	22s	-41%
`mld_ntt_butterfly_block`	✅	12s	23s	-48%
`sig_unpack_hints`	✅	11s	2s	+450%
`sign_signature_internal`	✅	11s	4s	+175%
`poly_ntt_c`	✅	10s	21s	-52%
`rej_uniform`	✅	10s	8s	+25%
`rej_uniform_c`	✅	10s	16s	-38%
`poly_uniform_eta_4x`	✅	9s	12s	-25%
`polyt0_unpack`	✅	9s	12s	-25%
`polyeta_unpack`	✅	8s	14s	-43%
`polyz_unpack_c`	✅	8s	8s	+0%
`rej_uniform_native_x86_64`	✅	8s	-	new
`polyvec_matrix_pointwise_montgomery_row`	✅	7s	6s	+17%
`mld_check_pct`	✅	6s	15s	-60%
`poly_invntt_tomont_c`	✅	6s	11s	-45%
`polyveck_invntt_tomont`	✅	6s	5s	+20%
`mld_keccakf1600_permute_c`	✅	5s	7s	-29%
`pointwise_native_x86_64`	✅	5s	4s	+25%
`poly_chknorm_c`	✅	5s	11s	-55%
`sign_keypair`	✅	5s	5s	+0%
`sign_signature`	✅	5s	6s	-17%
`unpack_sk_s2hat`	✅	5s	4s	+25%
`keccak_absorb_once_x4`	✅	4s	8s	-50%
`keccak_squeezeblocks_x4`	✅	4s	3s	+33%
`mld_compute_pack_z`	✅	4s	6s	-33%
`pack_sig_c`	✅	4s	5s	-20%
`poly_add`	✅	4s	7s	-43%
`poly_chknorm_native_aarch64`	✅	4s	2s	+100%
`poly_decompose_c`	✅	4s	5s	-20%
`poly_invntt_tomont_native`	✅	4s	3s	+33%
`poly_permute_bitrev_to_custom_optional`	✅	4s	5s	-20%
`poly_power2round`	✅	4s	4s	+0%
`polyt0_pack`	✅	4s	4s	+0%
`polyveck_chknorm`	✅	4s	67s	-94%
`polyveck_reduce`	✅	4s	4s	+0%
`polyw1_pack_88`	✅	4s	2s	+100%
`polyz_unpack`	✅	4s	3s	+33%
`rej_uniform_native`	✅	4s	5s	-20%
`shake256_release`	✅	4s	1s	+300%
`sign_signature_extmu`	✅	4s	4s	+0%
`unpack_pk_t1`	✅	4s	3s	+33%
`unpack_sk_s1hat`	✅	4s	3s	+33%
`intt_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	4s	-25%
`mld_sign_finish`	✅	3s	-	new
`mld_sign_resume`	✅	3s	-	new
`montgomery_reduce`	✅	3s	2s	+50%
`ntt_native_aarch64`	✅	3s	4s	-25%
`pack_sig_h`	✅	3s	4s	-25%
`pack_sk_s1`	✅	3s	3s	+0%
`pointwise_acc_native_x86_64`	✅	3s	4s	-25%
`poly_decompose_native_x86_64`	✅	3s	2s	+50%
`poly_ntt_native`	✅	3s	3s	+0%
`poly_pointwise_montgomery`	✅	3s	3s	+0%
`poly_uniform`	✅	3s	3s	+0%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	✅	3s	-	new
`polyvec_matrix_expand`	✅	3s	3s	+0%
`polyveck_ntt`	✅	3s	2s	+50%
`polyw1_pack`	✅	3s	4s	-25%
`polyw1_pack_32`	✅	3s	3s	+0%
`polyz_unpack_native`	✅	3s	3s	+0%
`rej_eta`	✅	3s	5s	-40%
`rej_uniform_eta_native_aarch64`	✅	3s	3s	+0%
`shake256_absorb`	✅	3s	2s	+50%
`shake256x4_absorb_once`	✅	3s	1s	+200%
`sign_signature_pre_hash_shake256`	✅	3s	4s	-25%
`sign_verify`	✅	3s	4s	-25%
`sign_verify_pre_hash_shake256`	✅	3s	5s	-40%
`sk_t0hat_get_poly`	✅	3s	1s	+200%
`unpack_sk_t0hat`	✅	3s	2s	+50%
`decompose`	✅	2s	3s	-33%
`fqscale`	✅	2s	2s	+0%
`keccak_absorb`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	✅	2s	4s	-50%
`keccakf1600_permute`	✅	2s	2s	+0%
`keccakf1600_permute_native`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	3s	-33%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	✅	2s	4s	-50%
`keccakf1600x4_permute`	✅	2s	4s	-50%
`keccakf1600x4_xor_bytes_native`	✅	2s	5s	-60%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mld_h`	✅	2s	4s	-50%
`mld_polymat_expand_entry`	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	✅	2s	3s	-33%
`mld_sample_s1_s2`	✅	2s	1s	+100%
`mld_sign_attempt`	✅	2s	-	new
`mld_value_barrier_i64`	✅	2s	3s	-33%
`mld_value_barrier_u32`	✅	2s	1s	+100%
`mld_value_barrier_u8`	✅	2s	4s	-50%
`ntt_native_x86_64`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	4s	-50%
`pack_sk_rho_key_tr_s2`	✅	2s	5s	-60%
`pointwise_acc_native_aarch64`	✅	2s	6s	-67%
`pointwise_native_aarch64`	✅	2s	2s	+0%
`poly_caddq`	✅	2s	4s	-50%
`poly_caddq_c`	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	✅	2s	4s	-50%
`poly_challenge`	✅	2s	6s	-67%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	✅	2s	2s	+0%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	✅	2s	4s	-50%
`poly_decompose_native`	✅	2s	2s	+0%
`poly_invntt_tomont`	✅	2s	2s	+0%
`poly_ntt`	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	2s	+0%
`poly_reduce`	✅	2s	4s	-50%
`poly_shiftl`	✅	2s	4s	-50%
`poly_uniform_4x`	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	✅	2s	5s	-60%
`poly_use_hint_c`	✅	2s	5s	-60%
`poly_use_hint_native`	✅	2s	3s	-33%
`polyeta_pack`	✅	2s	3s	-33%
`polyt1_pack`	✅	2s	3s	-33%
`polyt1_unpack`	✅	2s	2s	+0%
`polyvec_matrix_expand_serial`	✅	2s	4s	-50%
`polyveck_caddq`	✅	2s	3s	-33%
`polyveck_decompose`	✅	2s	7s	-71%
`polyveck_pack_eta`	✅	2s	4s	-50%
`polyveck_unpack_eta`	✅	2s	2s	+0%
`polyvecl_chknorm`	✅	2s	11s	-82%
`polyvecl_ntt`	✅	2s	3s	-33%
`polyvecl_pack_eta`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	3s	-33%
`polyvecl_unpack_eta`	✅	2s	4s	-50%
`reduce32`	✅	2s	3s	-33%
`rej_eta_c`	✅	2s	4s	-50%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native_aarch64`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	3s	-33%
`shake128_squeeze`	✅	2s	2s	+0%
`shake128x4_absorb_once`	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	✅	2s	2s	+0%
`shake256`	✅	2s	1s	+100%
`shake256_finalize`	✅	2s	2s	+0%
`shake256_init`	✅	2s	4s	-50%
`shake256_squeeze`	✅	2s	2s	+0%
`sign_signature_pre_hash_internal`	✅	2s	4s	-50%
`sign_verify_extmu`	✅	2s	5s	-60%
`sign_verify_pre_hash_internal`	✅	2s	5s	-60%
`sk_s2hat_get_poly`	✅	2s	5s	-60%
`sys_check_capability`	✅	2s	2s	+0%
`unpack_sk`	✅	2s	3s	-33%
`use_hint`	✅	2s	2s	+0%
`yvec_init`	✅	2s	1s	+100%
`caddq`	✅	1s	6s	-83%
`intt_native_x86_64`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	3s	-67%
`keccak_init`	✅	1s	3s	-67%
`keccak_squeeze`	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	1s	6s	-83%
`make_hint`	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	✅	1s	2s	-50%
`mld_ct_memcmp`	✅	1s	1s	+0%
`mld_ct_sel_int32`	✅	1s	3s	-67%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	1s	4s	-75%
`mld_sample_s1_s2_serial`	✅	1s	4s	-75%
`pack_sig_z`	✅	1s	2s	-50%
`poly_caddq_native`	✅	1s	3s	-67%
`poly_caddq_native_aarch64`	✅	1s	3s	-67%
`poly_chknorm_native`	✅	1s	4s	-75%
`poly_decompose_88_native_aarch64`	✅	1s	3s	-67%
`poly_sub`	✅	1s	3s	-67%
`poly_uniform_eta`	✅	1s	2s	-50%
`poly_use_hint`	✅	1s	2s	-50%
`poly_use_hint_native_aarch64`	✅	1s	3s	-67%
`polyveck_pack_w1`	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_c`	✅	1s	4s	-75%
`polyvecl_uniform_gamma1`	✅	1s	2s	-50%
`polyvecl_uniform_gamma1_serial`	✅	1s	2s	-50%
`polyvecl_unpack_z`	✅	1s	3s	-67%
`polyz_pack`	✅	1s	2s	-50%
`polyz_unpack_17_native_aarch64`	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	✅	1s	4s	-75%
`polyz_unpack_native_x86_64`	✅	1s	3s	-67%
`power2round`	✅	1s	2s	-50%
`rej_eta_native`	✅	1s	3s	-67%
`shake128_finalize`	✅	1s	3s	-67%
`shake128_init`	✅	1s	2s	-50%
`shake128_release`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sk_s1hat_get_poly`	✅	1s	2s	-50%
`yvec_get_poly`	✅	1s	3s	-67%

oqs-bot · 2026-08-11T06:01:17Z

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	98s	50s	+96%
`mld_attempt_signature_generation`	⚠️	295s	58s	+409%
`sig_unpack_hints`	⚠️	22s	2s	+1000%
`sign_keypair_internal`	⚠️	22s	4s	+450%
`sign_pk_from_sk`	⚠️	37s	5s	+640%
`sign_signature_internal`	⚠️	93s	26s	+258%
`sign_verify_internal`	⚠️	287s	114s	+152%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1789s	1514s	+18.2%
`mld_attempt_signature_generation`	⚠️	295s	58s	+409%
`sign_verify_internal`	⚠️	287s	114s	+152%
`polyvecl_pointwise_acc_montgomery_c`	✅	148s	131s	+13%
`poly_pointwise_montgomery_c`	✅	139s	114s	+22%
`compute_pack_t0_t1`	⚠️	98s	50s	+96%
`sign_signature_internal`	⚠️	93s	26s	+258%
`mld_invntt_layer`	✅	57s	107s	-47%
`sign_pk_from_sk`	⚠️	37s	5s	+640%
`fqmul`	✅	24s	39s	-38%
`sig_unpack_hints`	⚠️	22s	2s	+1000%
`sign_keypair_internal`	⚠️	22s	4s	+450%
`mld_ntt_layer`	✅	21s	42s	-50%
`polyvec_matrix_expand`	✅	18s	28s	-36%
`keccakf1600x4_permute_native`	✅	11s	22s	-50%
`mld_ntt_butterfly_block`	✅	10s	23s	-57%
`poly_ntt_c`	✅	10s	19s	-47%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	9s	15s	-40%
`rej_uniform_native_x86_64`	✅	9s	-	new
`poly_chknorm_c`	✅	8s	17s	-53%
`polyt0_unpack`	✅	8s	15s	-47%
`rej_uniform`	✅	8s	18s	-56%
`poly_uniform_eta_4x`	✅	7s	11s	-36%
`polyeta_unpack`	✅	7s	14s	-50%
`mld_keccakf1600_permute_c`	✅	6s	8s	-25%
`poly_uniform_4x`	✅	6s	14s	-57%
`polyvecl_ntt`	✅	6s	2s	+200%
`sign_keypair`	✅	6s	4s	+50%
`sign_signature_pre_hash_shake256`	✅	6s	3s	+100%
`intt_native_x86_64`	✅	5s	4s	+25%
`mld_compute_pack_z`	✅	5s	7s	-29%
`poly_invntt_tomont_c`	✅	5s	11s	-55%
`polyz_unpack_17_native_aarch64`	✅	5s	5s	+0%
`polyz_unpack_c`	✅	5s	11s	-55%
`rej_uniform_c`	✅	5s	15s	-67%
`keccak_absorb_once_x4`	✅	4s	9s	-56%
`keccakf1600_permute`	✅	4s	2s	+100%
`mld_check_pct`	✅	4s	14s	-71%
`mld_sign_finish`	✅	4s	-	new
`poly_uniform_gamma1`	✅	4s	4s	+0%
`poly_use_hint_native_aarch64`	✅	4s	2s	+100%
`polyz_unpack_native_x86_64`	✅	4s	3s	+33%
`reduce32`	✅	4s	2s	+100%
`sign_verify_pre_hash_shake256`	✅	4s	5s	-20%
`unpack_pk_t1`	✅	4s	5s	-20%
`unpack_sk_t0hat`	✅	4s	3s	+33%
`decompose`	✅	3s	2s	+50%
`fqscale`	✅	3s	3s	+0%
`keccak_absorb`	✅	3s	5s	-40%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	1s	+200%
`keccak_squeeze`	✅	3s	1s	+200%
`keccakf1600_extract_bytes (big endian)`	✅	3s	2s	+50%
`keccakf1600_permute_native`	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	✅	3s	1s	+200%
`keccakf1600x4_extract_bytes_native`	✅	3s	3s	+0%
`keccakf1600x4_xor_bytes`	✅	3s	2s	+50%
`make_hint`	✅	3s	3s	+0%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	✅	3s	1s	+200%
`mld_keccakf1600_extract_bytes`	✅	3s	2s	+50%
`mld_polymat_expand_entry`	✅	3s	3s	+0%
`nttunpack_native_x86_64`	✅	3s	1s	+200%
`pointwise_acc_native_x86_64`	✅	3s	7s	-57%
`pointwise_native_aarch64`	✅	3s	5s	-40%
`poly_caddq_c`	✅	3s	2s	+50%
`poly_chknorm_native_aarch64`	✅	3s	4s	-25%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_decompose_native`	✅	3s	3s	+0%
`poly_decompose_native_x86_64`	✅	3s	3s	+0%
`poly_pointwise_montgomery`	✅	3s	3s	+0%
`poly_power2round`	✅	3s	4s	-25%
`poly_uniform`	✅	3s	6s	-50%
`poly_uniform_eta`	✅	3s	5s	-40%
`poly_uniform_gamma1_4x`	✅	3s	5s	-40%
`poly_use_hint_c`	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	✅	3s	-	new
`polyt1_pack`	✅	3s	4s	-25%
`polyvec_matrix_expand_serial`	✅	3s	8s	-62%
`polyveck_caddq`	✅	3s	3s	+0%
`polyveck_decompose`	✅	3s	4s	-25%
`polyveck_pack_eta`	✅	3s	2s	+50%
`polyveck_unpack_eta`	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	2s	+50%
`polyvecl_unpack_z`	✅	3s	2s	+50%
`polyw1_pack_32`	✅	3s	2s	+50%
`power2round`	✅	3s	3s	+0%
`rej_eta`	✅	3s	3s	+0%
`rej_uniform_eta_native_x86_64`	✅	3s	-	new
`shake256_init`	✅	3s	3s	+0%
`sign_signature_extmu`	✅	3s	4s	-25%
`sign_signature_pre_hash_internal`	✅	3s	6s	-50%
`sk_t0hat_get_poly`	✅	3s	2s	+50%
`sys_check_capability`	✅	3s	4s	-25%
`intt_native_aarch64`	✅	2s	9s	-78%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_init`	✅	2s	3s	-33%
`keccak_squeezeblocks_x4`	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	✅	2s	3s	-33%
`mld_ct_memcmp`	✅	2s	3s	-33%
`mld_h`	✅	2s	4s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	✅	2s	4s	-50%
`mld_sample_s1_s2`	✅	2s	4s	-50%
`mld_sample_s1_s2_serial`	✅	2s	3s	-33%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`mld_value_barrier_u8`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	2s	+0%
`pack_sig_h`	✅	2s	3s	-33%
`pack_sig_z`	✅	2s	4s	-50%
`pack_sk_s1`	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	✅	2s	4s	-50%
`poly_add`	✅	2s	7s	-71%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	✅	2s	4s	-50%
`poly_chknorm`	✅	2s	4s	-50%
`poly_decompose`	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	✅	2s	4s	-50%
`poly_decompose_c`	✅	2s	4s	-50%
`poly_ntt`	✅	2s	3s	-33%
`poly_ntt_native`	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_pointwise_montgomery_native`	✅	2s	2s	+0%
`poly_reduce`	✅	2s	3s	-33%
`poly_sub`	✅	2s	3s	-33%
`poly_use_hint`	✅	2s	4s	-50%
`poly_use_hint_native`	✅	2s	4s	-50%
`polyt0_pack`	✅	2s	2s	+0%
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	2s	+0%
`polyveck_chknorm`	✅	2s	5s	-60%
`polyveck_invntt_tomont`	✅	2s	5s	-60%
`polyveck_ntt`	✅	2s	5s	-60%
`polyveck_pack_w1`	✅	2s	1s	+100%
`polyvecl_chknorm`	✅	2s	10s	-80%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	4s	-50%
`polyvecl_uniform_gamma1`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	✅	2s	2s	+0%
`polyvecl_unpack_eta`	✅	2s	2s	+0%
`polyw1_pack`	✅	2s	3s	-33%
`polyw1_pack_88`	✅	2s	1s	+100%
`polyz_pack`	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`rej_eta_c`	✅	2s	4s	-50%
`rej_eta_native`	✅	2s	6s	-67%
`rej_uniform_eta_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native`	✅	2s	4s	-50%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_finalize`	✅	2s	2s	+0%
`shake128_init`	✅	2s	3s	-33%
`shake128_squeeze`	✅	2s	1s	+100%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake256_absorb`	✅	2s	3s	-33%
`shake256_release`	✅	2s	2s	+0%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	✅	2s	4s	-50%
`sign_signature`	✅	2s	3s	-33%
`sign_verify_extmu`	✅	2s	3s	-33%
`sign_verify_pre_hash_internal`	✅	2s	3s	-33%
`sk_s1hat_get_poly`	✅	2s	3s	-33%
`unpack_sk`	✅	2s	3s	-33%
`unpack_sk_s1hat`	✅	2s	1s	+100%
`unpack_sk_s2hat`	✅	2s	4s	-50%
`use_hint`	✅	2s	2s	+0%
`yvec_init`	✅	2s	3s	-33%
`caddq`	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_f1600_x4_native_avx2`	✅	1s	3s	-67%
`keccak_finalize`	✅	1s	3s	-67%
`keccakf1600_xor_bytes (big endian)`	✅	1s	4s	-75%
`keccakf1600x4_permute`	✅	1s	4s	-75%
`mld_ct_cmask_neg_i32`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	✅	1s	4s	-75%
`mld_ct_get_optblocker_u8`	✅	1s	1s	+0%
`mld_ct_sel_int32`	✅	1s	2s	-50%
`mld_sign_attempt`	✅	1s	-	new
`mld_sign_resume`	✅	1s	-	new
`mld_value_barrier_u32`	✅	1s	2s	-50%
`montgomery_reduce`	✅	1s	3s	-67%
`ntt_native_x86_64`	✅	1s	3s	-67%
`pack_sk_rho_key_tr_s2`	✅	1s	3s	-67%
`pointwise_native_x86_64`	✅	1s	4s	-75%
`poly_caddq_native`	✅	1s	5s	-80%
`poly_caddq_native_x86_64`	✅	1s	4s	-75%
`poly_challenge`	✅	1s	3s	-67%
`poly_chknorm_native`	✅	1s	4s	-75%
`poly_decompose_32_native_aarch64`	✅	1s	2s	-50%
`poly_invntt_tomont`	✅	1s	4s	-75%
`poly_invntt_tomont_native`	✅	1s	4s	-75%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	4s	-75%
`poly_shiftl`	✅	1s	3s	-67%
`polyeta_pack`	✅	1s	3s	-67%
`polyt1_unpack`	✅	1s	5s	-80%
`polyveck_reduce`	✅	1s	5s	-80%
`polyz_unpack`	✅	1s	3s	-67%
`polyz_unpack_native`	✅	1s	2s	-50%
`rej_uniform_native_aarch64`	✅	1s	5s	-80%
`shake128_release`	✅	1s	1s	+0%
`shake128x4_squeezeblocks`	✅	1s	1s	+0%
`shake256`	✅	1s	1s	+0%
`shake256_finalize`	✅	1s	2s	-50%
`sign_verify`	✅	1s	4s	-75%
`sk_s2hat_get_poly`	✅	1s	2s	-50%
`yvec_get_poly`	✅	1s	3s	-67%

oqs-bot · 2026-08-11T06:01:18Z

CBMC Results (ML-DSA-87, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	28s	12s	+133%
`mld_attempt_signature_generation`	⚠️	230s	34s	+576%
`sign_keypair_internal`	⚠️	45s	6s	+650%
`sign_pk_from_sk`	⚠️	56s	6s	+833%
`sign_verify_internal`	⚠️	299s	47s	+536%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1593s	1436s	+10.9%
`sign_verify_internal`	⚠️	299s	47s	+536%
`mld_attempt_signature_generation`	⚠️	230s	34s	+576%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	186s	196s	-5%
`poly_pointwise_montgomery_c`	✅	64s	125s	-49%
`sign_pk_from_sk`	⚠️	56s	6s	+833%
`mld_invntt_layer`	✅	54s	111s	-51%
`sign_keypair_internal`	⚠️	45s	6s	+650%
`compute_pack_t0_t1`	⚠️	28s	12s	+133%
`fqmul`	✅	23s	39s	-41%
`mld_ntt_layer`	✅	21s	44s	-52%
`sig_unpack_hints`	✅	13s	4s	+225%
`sign_signature_internal`	✅	13s	3s	+333%
`keccakf1600x4_permute_native`	✅	12s	25s	-52%
`mld_ntt_butterfly_block`	✅	11s	23s	-52%
`rej_uniform_c`	✅	10s	18s	-44%
`poly_ntt_c`	✅	9s	19s	-53%
`poly_uniform_eta_4x`	✅	9s	12s	-25%
`polyt0_unpack`	✅	9s	14s	-36%
`polyeta_unpack`	✅	8s	13s	-38%
`keccak_absorb_once_x4`	✅	7s	8s	-12%
`poly_invntt_tomont_c`	✅	7s	9s	-22%
`polyveck_decompose`	✅	7s	12s	-42%
`rej_uniform`	✅	7s	7s	+0%
`poly_chknorm_c`	✅	6s	13s	-54%
`polyvecl_chknorm`	✅	6s	38s	-84%
`polyvecl_ntt`	✅	6s	8s	-25%
`rej_uniform_native_x86_64`	✅	6s	-	new
`sign_signature_pre_hash_internal`	✅	6s	2s	+200%
`mld_sample_s1_s2`	✅	5s	8s	-38%
`mld_sample_s1_s2_serial`	✅	5s	6s	-17%
`pointwise_acc_native_x86_64`	✅	5s	8s	-38%
`poly_permute_bitrev_to_custom_optional_native`	✅	5s	3s	+67%
`polyveck_caddq`	✅	5s	8s	-38%
`polyveck_invntt_tomont`	✅	5s	4s	+25%
`polyz_unpack_c`	✅	5s	7s	-29%
`rej_eta_native`	✅	5s	4s	+25%
`sk_s1hat_get_poly`	✅	5s	3s	+67%
`unpack_sk_s2hat`	✅	5s	3s	+67%
`keccak_absorb`	✅	4s	4s	+0%
`keccak_squeezeblocks_x4`	✅	4s	4s	+0%
`keccakf1600_permute_native`	✅	4s	3s	+33%
`mld_check_pct`	✅	4s	15s	-73%
`mld_compute_pack_z`	✅	4s	6s	-33%
`mld_ct_cmask_neg_i32`	✅	4s	2s	+100%
`mld_ct_sel_int32`	✅	4s	2s	+100%
`mld_h`	✅	4s	2s	+100%
`mld_value_barrier_u32`	✅	4s	3s	+33%
`ntt_native_aarch64`	✅	4s	4s	+0%
`poly_caddq`	✅	4s	5s	-20%
`poly_chknorm`	✅	4s	4s	+0%
`poly_invntt_tomont`	✅	4s	4s	+0%
`polyvec_matrix_expand_serial`	✅	4s	3s	+33%
`polyvec_matrix_pointwise_montgomery_row`	✅	4s	13s	-69%
`polyveck_reduce`	✅	4s	6s	-33%
`sign_keypair`	✅	4s	4s	+0%
`sign_signature`	✅	4s	4s	+0%
`sign_verify_pre_hash_shake256`	✅	4s	7s	-43%
`yvec_init`	✅	4s	4s	+0%
`fqscale`	✅	3s	1s	+200%
`intt_native_x86_64`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	1s	+200%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	2s	+50%
`keccak_squeeze`	✅	3s	5s	-40%
`keccakf1600_permute`	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	✅	3s	2s	+50%
`make_hint`	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u32`	✅	3s	5s	-40%
`mld_keccakf1600_permute_c`	✅	3s	8s	-62%
`mld_value_barrier_u8`	✅	3s	2s	+50%
`montgomery_reduce`	✅	3s	2s	+50%
`pack_sig_h`	✅	3s	3s	+0%
`pack_sk_s1`	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	✅	3s	5s	-40%
`poly_caddq_native_aarch64`	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	✅	3s	3s	+0%
`poly_decompose`	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	3s	+0%
`poly_reduce`	✅	3s	4s	-25%
`poly_uniform_4x`	✅	3s	3s	+0%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint_c`	✅	3s	4s	-25%
`polyeta_pack`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	9s	-67%
`polyveck_unpack_eta`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	✅	3s	2s	+50%
`polyvecl_unpack_eta`	✅	3s	3s	+0%
`polyz_pack`	✅	3s	4s	-25%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	✅	3s	4s	-25%
`reduce32`	✅	3s	3s	+0%
`shake256x4_absorb_once`	✅	3s	5s	-40%
`sign_signature_extmu`	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	✅	3s	3s	+0%
`sign_verify_extmu`	✅	3s	4s	-25%
`sign_verify_pre_hash_internal`	✅	3s	3s	+0%
`unpack_sk`	✅	3s	4s	-25%
`yvec_get_poly`	✅	3s	2s	+50%
`caddq`	✅	2s	3s	-33%
`decompose`	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	1s	+100%
`keccak_init`	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes`	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	✅	2s	4s	-50%
`keccakf1600x4_xor_bytes`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`mld_ct_abs_i32`	✅	2s	1s	+100%
`mld_ct_get_optblocker_i64`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	1s	+100%
`mld_prepare_domain_separation_prefix`	✅	2s	3s	-33%
`mld_sign_attempt`	✅	2s	-	new
`mld_sign_finish`	✅	2s	-	new
`mld_value_barrier_i64`	✅	2s	2s	+0%
`ntt_native_x86_64`	✅	2s	2s	+0%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	2s	+0%
`pack_sig_z`	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	✅	2s	2s	+0%
`pointwise_native_aarch64`	✅	2s	4s	-50%
`pointwise_native_x86_64`	✅	2s	5s	-60%
`poly_add`	✅	2s	8s	-75%
`poly_caddq_c`	✅	2s	3s	-33%
`poly_caddq_native`	✅	2s	3s	-33%
`poly_chknorm_native_aarch64`	✅	2s	5s	-60%
`poly_chknorm_native_x86_64`	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_c`	✅	2s	6s	-67%
`poly_invntt_tomont_native`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_power2round`	✅	2s	7s	-71%
`poly_shiftl`	✅	2s	4s	-50%
`poly_sub`	✅	2s	5s	-60%
`poly_uniform`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	4s	-50%
`poly_use_hint_native_x86_64`	✅	2s	-	new
`polyt0_pack`	✅	2s	3s	-33%
`polyt1_pack`	✅	2s	5s	-60%
`polyt1_unpack`	✅	2s	3s	-33%
`polyvec_matrix_expand`	✅	2s	3s	-33%
`polyveck_ntt`	✅	2s	3s	-33%
`polyveck_pack_eta`	✅	2s	5s	-60%
`polyveck_pack_w1`	✅	2s	3s	-33%
`polyvecl_pack_eta`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyw1_pack_32`	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`polyz_unpack_native`	✅	2s	1s	+100%
`polyz_unpack_native_x86_64`	✅	2s	3s	-33%
`power2round`	✅	2s	3s	-33%
`rej_eta`	✅	2s	2s	+0%
`rej_eta_c`	✅	2s	4s	-50%
`rej_uniform_eta_native_aarch64`	✅	2s	3s	-33%
`rej_uniform_native`	✅	2s	5s	-60%
`rej_uniform_native_aarch64`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_init`	✅	2s	2s	+0%
`shake128_squeeze`	✅	2s	1s	+100%
`shake128x4_absorb_once`	✅	2s	4s	-50%
`shake256x4_squeezeblocks`	✅	2s	4s	-50%
`sign_verify`	✅	2s	2s	+0%
`sk_t0hat_get_poly`	✅	2s	3s	-33%
`unpack_pk_t1`	✅	2s	2s	+0%
`unpack_sk_s1hat`	✅	2s	3s	-33%
`unpack_sk_t0hat`	✅	2s	4s	-50%
`intt_native_aarch64`	✅	1s	4s	-75%
`keccak_f1600_x1_native_aarch64`	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	2s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	1s	3s	-67%
`keccakf1600x4_permute`	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u8`	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	✅	1s	3s	-67%
`mld_ct_memcmp`	✅	1s	1s	+0%
`mld_keccakf1600_extract_bytes`	✅	1s	1s	+0%
`mld_keccakf1600x4_extract_bytes_c`	✅	1s	3s	-67%
`mld_polymat_expand_entry`	✅	1s	4s	-75%
`mld_sign_resume`	✅	1s	-	new
`poly_challenge`	✅	1s	4s	-75%
`poly_chknorm_native`	✅	1s	1s	+0%
`poly_decompose_native`	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	✅	1s	3s	-67%
`poly_ntt`	✅	1s	2s	-50%
`poly_pointwise_montgomery`	✅	1s	3s	-67%
`poly_uniform_eta`	✅	1s	5s	-80%
`poly_uniform_gamma1_4x`	✅	1s	3s	-67%
`poly_use_hint_native`	✅	1s	1s	+0%
`poly_use_hint_native_aarch64`	✅	1s	3s	-67%
`polyvecl_uniform_gamma1`	✅	1s	3s	-67%
`polyvecl_unpack_z`	✅	1s	3s	-67%
`polyw1_pack`	✅	1s	2s	-50%
`polyw1_pack_88`	✅	1s	2s	-50%
`rej_uniform_eta_native_x86_64`	✅	1s	-	new
`shake128_finalize`	✅	1s	2s	-50%
`shake128_release`	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	✅	1s	1s	+0%
`shake256`	✅	1s	3s	-67%
`shake256_absorb`	✅	1s	3s	-67%
`shake256_finalize`	✅	1s	3s	-67%
`shake256_init`	✅	1s	3s	-67%
`shake256_release`	✅	1s	5s	-80%
`shake256_squeeze`	✅	1s	2s	-50%
`sk_s2hat_get_poly`	✅	1s	2s	-50%
`sys_check_capability`	✅	1s	2s	-50%
`use_hint`	✅	1s	3s	-67%

oqs-bot · 2026-08-11T06:02:26Z

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	126s	13s	+869%
`mld_attempt_signature_generation`	⚠️	252s	63s	+300%
`sig_unpack_hints`	⚠️	25s	2s	+1150%
`sign_keypair_internal`	⚠️	24s	5s	+380%
`sign_pk_from_sk`	⚠️	41s	6s	+583%
`sign_signature_internal`	⚠️	189s	55s	+244%
`sign_verify_internal`	⚠️	389s	177s	+120%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2093s	1784s	+17.3%
`sign_verify_internal`	⚠️	389s	177s	+120%
`mld_attempt_signature_generation`	⚠️	252s	63s	+300%
`sign_signature_internal`	⚠️	189s	55s	+244%
`polyvecl_pointwise_acc_montgomery_c`	✅	166s	210s	-21%
`poly_pointwise_montgomery_c`	✅	133s	125s	+6%
`compute_pack_t0_t1`	⚠️	126s	13s	+869%
`polyvec_matrix_expand`	✅	72s	110s	-35%
`mld_invntt_layer`	✅	57s	109s	-48%
`sign_pk_from_sk`	⚠️	41s	6s	+583%
`sig_unpack_hints`	⚠️	25s	2s	+1150%
`fqmul`	✅	24s	40s	-40%
`sign_keypair_internal`	⚠️	24s	5s	+380%
`mld_ntt_layer`	✅	21s	41s	-49%
`polyvec_matrix_expand_serial`	✅	17s	27s	-37%
`polyveck_ntt`	✅	15s	7s	+114%
`mld_ntt_butterfly_block`	✅	13s	24s	-46%
`polyveck_decompose`	✅	12s	12s	+0%
`keccakf1600x4_permute_native`	✅	11s	23s	-52%
`poly_ntt_c`	✅	10s	19s	-47%
`polyt0_unpack`	✅	10s	16s	-38%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	9s	18s	-50%
`rej_uniform_native_x86_64`	✅	9s	-	new
`rej_uniform`	✅	8s	18s	-56%
`poly_uniform_4x`	✅	7s	13s	-46%
`rej_uniform_c`	✅	7s	14s	-50%
`poly_chknorm_c`	✅	6s	15s	-60%
`poly_invntt_tomont_c`	✅	6s	11s	-45%
`poly_uniform_eta_4x`	✅	6s	14s	-57%
`polyz_unpack_c`	✅	6s	13s	-54%
`sign_keypair`	✅	6s	3s	+100%
`mld_check_pct`	✅	5s	14s	-64%
`mld_keccakf1600_permute_c`	✅	5s	6s	-17%
`mld_prepare_domain_separation_prefix`	✅	5s	2s	+150%
`poly_power2round`	✅	5s	4s	+25%
`polyt0_pack`	✅	5s	3s	+67%
`polyveck_caddq`	✅	5s	6s	-17%
`rej_uniform_native`	✅	5s	4s	+25%
`keccak_absorb_once_x4`	✅	4s	8s	-50%
`keccak_squeezeblocks_x4`	✅	4s	5s	-20%
`make_hint`	✅	4s	2s	+100%
`mld_ct_memcmp`	✅	4s	2s	+100%
`pointwise_acc_native_aarch64`	✅	4s	6s	-33%
`poly_decompose_c`	✅	4s	5s	-20%
`poly_uniform_eta`	✅	4s	4s	+0%
`polyvecl_ntt`	✅	4s	4s	+0%
`polyvecl_uniform_gamma1`	✅	4s	2s	+100%
`polyvecl_unpack_eta`	✅	4s	3s	+33%
`rej_uniform_eta_native_aarch64`	✅	4s	4s	+0%
`shake128x4_squeezeblocks`	✅	4s	3s	+33%
`sign_signature`	✅	4s	6s	-33%
`sign_verify_pre_hash_internal`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	5s	-20%
`sk_s1hat_get_poly`	✅	4s	6s	-33%
`unpack_pk_t1`	✅	4s	5s	-20%
`caddq`	✅	3s	3s	+0%
`fqscale`	✅	3s	3s	+0%
`keccak_absorb`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	2s	+50%
`keccakf1600_permute`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	✅	3s	4s	-25%
`keccakf1600x4_permute`	✅	3s	4s	-25%
`keccakf1600x4_xor_bytes`	✅	3s	1s	+200%
`mld_compute_pack_z`	✅	3s	7s	-57%
`mld_polymat_expand_entry`	✅	3s	4s	-25%
`mld_sample_s1_s2`	✅	3s	6s	-50%
`mld_sample_s1_s2_serial`	✅	3s	4s	-25%
`mld_sign_attempt`	✅	3s	-	new
`mld_value_barrier_i64`	✅	3s	2s	+50%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`ntt_native_aarch64`	✅	3s	2s	+50%
`nttunpack_native_x86_64`	✅	3s	3s	+0%
`pack_sk_rho_key_tr_s2`	✅	3s	2s	+50%
`pack_sk_s1`	✅	3s	5s	-40%
`pointwise_acc_native_x86_64`	✅	3s	8s	-62%
`poly_add`	✅	3s	9s	-67%
`poly_caddq`	✅	3s	2s	+50%
`poly_caddq_c`	✅	3s	2s	+50%
`poly_invntt_tomont`	✅	3s	3s	+0%
`polyeta_pack`	✅	3s	3s	+0%
`polyt1_pack`	✅	3s	3s	+0%
`polyveck_invntt_tomont`	✅	3s	8s	-62%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	✅	3s	3s	+0%
`polyw1_pack_32`	✅	3s	4s	-25%
`polyz_pack`	✅	3s	3s	+0%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_native_x86_64`	✅	3s	3s	+0%
`reduce32`	✅	3s	3s	+0%
`rej_eta_native`	✅	3s	3s	+0%
`shake256_absorb`	✅	3s	2s	+50%
`shake256_init`	✅	3s	2s	+50%
`shake256_squeeze`	✅	3s	3s	+0%
`sign_signature_extmu`	✅	3s	2s	+50%
`sign_signature_pre_hash_internal`	✅	3s	3s	+0%
`sign_verify`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	2s	+50%
`unpack_sk`	✅	3s	3s	+0%
`unpack_sk_s1hat`	✅	3s	2s	+50%
`unpack_sk_t0hat`	✅	3s	5s	-40%
`yvec_init`	✅	3s	3s	+0%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	4s	-50%
`keccakf1600_xor_bytes`	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	4s	-50%
`mld_ct_abs_i32`	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	3s	-33%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_h`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	1s	+100%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	3s	-33%
`mld_sign_resume`	✅	2s	-	new
`ntt_native_x86_64`	✅	2s	2s	+0%
`pack_sig_c`	✅	2s	5s	-60%
`pack_sig_h`	✅	2s	5s	-60%
`pointwise_native_x86_64`	✅	2s	3s	-33%
`poly_caddq_native`	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	✅	2s	3s	-33%
`poly_challenge`	✅	2s	6s	-67%
`poly_chknorm_native_aarch64`	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	✅	2s	1s	+100%
`poly_decompose_native_x86_64`	✅	2s	3s	-33%
`poly_invntt_tomont_native`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_pointwise_montgomery`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	3s	-33%
`poly_reduce`	✅	2s	3s	-33%
`poly_shiftl`	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	✅	2s	4s	-50%
`poly_use_hint_c`	✅	2s	5s	-60%
`poly_use_hint_native`	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	✅	2s	-	new
`polyeta_unpack`	✅	2s	8s	-75%
`polyt1_unpack`	✅	2s	5s	-60%
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	1s	+100%
`polyveck_chknorm`	✅	2s	6s	-67%
`polyveck_unpack_eta`	✅	2s	6s	-67%
`polyvecl_chknorm`	✅	2s	7s	-71%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyw1_pack`	✅	2s	4s	-50%
`polyw1_pack_88`	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	✅	2s	3s	-33%
`polyz_unpack_native`	✅	2s	4s	-50%
`rej_eta_c`	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`shake128_finalize`	✅	2s	1s	+100%
`shake128_init`	✅	2s	2s	+0%
`shake128_squeeze`	✅	2s	2s	+0%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake256`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`sign_signature_pre_hash_shake256`	✅	2s	3s	-33%
`sign_verify_extmu`	✅	2s	3s	-33%
`sk_s2hat_get_poly`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_sk_s2hat`	✅	2s	4s	-50%
`yvec_get_poly`	✅	2s	3s	-33%
`decompose`	✅	1s	1s	+0%
`intt_native_aarch64`	✅	1s	3s	-67%
`intt_native_x86_64`	✅	1s	3s	-67%
`keccak_f1600_x1_native_aarch64`	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	2s	-50%
`keccak_finalize`	✅	1s	2s	-50%
`keccak_init`	✅	1s	1s	+0%
`keccakf1600_permute_native`	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	✅	1s	4s	-75%
`mld_ct_cmask_nonzero_u8`	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	✅	1s	2s	-50%
`mld_sign_finish`	✅	1s	-	new
`mld_value_barrier_u32`	✅	1s	3s	-67%
`montgomery_reduce`	✅	1s	4s	-75%
`pack_sig_z`	✅	1s	2s	-50%
`pointwise_native_aarch64`	✅	1s	5s	-80%
`poly_caddq_native_aarch64`	✅	1s	2s	-50%
`poly_chknorm`	✅	1s	4s	-75%
`poly_chknorm_native`	✅	1s	2s	-50%
`poly_decompose`	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	✅	1s	3s	-67%
`poly_decompose_native`	✅	1s	3s	-67%
`poly_ntt`	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	4s	-75%
`poly_sub`	✅	1s	3s	-67%
`poly_uniform`	✅	1s	4s	-75%
`poly_uniform_gamma1`	✅	1s	3s	-67%
`poly_use_hint`	✅	1s	3s	-67%
`polyveck_pack_eta`	✅	1s	4s	-75%
`polyveck_pack_w1`	✅	1s	3s	-67%
`polyveck_reduce`	✅	1s	4s	-75%
`polyvecl_unpack_z`	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	✅	1s	3s	-67%
`power2round`	✅	1s	1s	+0%
`rej_eta`	✅	1s	2s	-50%
`rej_uniform_native_aarch64`	✅	1s	3s	-67%
`shake128_absorb`	✅	1s	2s	-50%
`shake128_release`	✅	1s	3s	-67%
`shake256_finalize`	✅	1s	1s	+0%
`shake256_release`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`use_hint`	✅	1s	2s	-50%

oqs-bot · 2026-08-11T06:07:52Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2761s	2151s	+28.4%
`compute_pack_t0_t1`	⚠️	191s	19s	+905%
`mld_attempt_signature_generation`	⚠️	288s	55s	+424%
`sig_unpack_hints`	⚠️	28s	3s	+833%
`sign_keypair_internal`	⚠️	51s	6s	+750%
`sign_pk_from_sk`	⚠️	47s	6s	+683%
`sign_signature_internal`	⚠️	325s	42s	+674%
`sign_verify_internal`	⚠️	723s	97s	+645%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2761s	2151s	+28.4%
`sign_verify_internal`	⚠️	723s	97s	+645%
`sign_signature_internal`	⚠️	325s	42s	+674%
`mld_attempt_signature_generation`	⚠️	288s	55s	+424%
`polyvecl_pointwise_acc_montgomery_c`	✅	213s	353s	-40%
`compute_pack_t0_t1`	⚠️	191s	19s	+905%
`poly_pointwise_montgomery_c`	✅	135s	144s	-6%
`polyvec_matrix_expand`	✅	81s	324s	-75%
`mld_invntt_layer`	✅	57s	115s	-50%
`sign_keypair_internal`	⚠️	51s	6s	+750%
`sign_pk_from_sk`	⚠️	47s	6s	+683%
`sig_unpack_hints`	⚠️	28s	3s	+833%
`fqmul`	✅	22s	43s	-49%
`mld_ntt_layer`	✅	22s	45s	-51%
`polyvec_matrix_expand_serial`	✅	21s	38s	-45%
`keccakf1600x4_permute_native`	✅	13s	23s	-43%
`mld_ntt_butterfly_block`	✅	10s	24s	-58%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	10s	18s	-44%
`poly_ntt_c`	✅	9s	21s	-57%
`polyt0_unpack`	✅	9s	14s	-36%
`rej_uniform_native_x86_64`	✅	8s	-	new
`poly_uniform_eta_4x`	✅	7s	11s	-36%
`rej_uniform`	✅	7s	15s	-53%
`rej_uniform_c`	✅	7s	19s	-63%
`sign_keypair`	✅	7s	4s	+75%
`mld_check_pct`	✅	6s	16s	-62%
`mld_keccakf1600_permute_c`	✅	6s	7s	-14%
`mld_sample_s1_s2`	✅	6s	6s	+0%
`poly_chknorm_c`	✅	6s	15s	-60%
`poly_uniform_4x`	✅	6s	13s	-54%
`polyeta_unpack`	✅	6s	17s	-65%
`polyveck_decompose`	✅	6s	13s	-54%
`pointwise_acc_native_aarch64`	✅	5s	6s	-17%
`poly_invntt_tomont_c`	✅	5s	12s	-58%
`poly_use_hint_native_x86_64`	✅	5s	-	new
`polyveck_caddq`	✅	5s	8s	-38%
`polyveck_chknorm`	✅	5s	3s	+67%
`polyveck_ntt`	✅	5s	11s	-55%
`polyz_unpack_c`	✅	5s	3s	+67%
`unpack_sk_s2hat`	✅	5s	3s	+67%
`keccak_absorb`	✅	4s	3s	+33%
`keccak_absorb_once_x4`	✅	4s	9s	-56%
`mld_compute_pack_z`	✅	4s	8s	-50%
`mld_ct_memcmp`	✅	4s	3s	+33%
`mld_polymat_expand_entry`	✅	4s	3s	+33%
`mld_sample_s1_s2_serial`	✅	4s	8s	-50%
`mld_sign_attempt`	✅	4s	-	new
`poly_caddq`	✅	4s	2s	+100%
`poly_decompose`	✅	4s	3s	+33%
`poly_decompose_c`	✅	4s	5s	-20%
`poly_ntt_native`	✅	4s	3s	+33%
`polyt1_pack`	✅	4s	3s	+33%
`polyveck_invntt_tomont`	✅	4s	9s	-56%
`polyvecl_ntt`	✅	4s	7s	-43%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	3s	+33%
`polyvecl_unpack_z`	✅	4s	4s	+0%
`shake256_squeeze`	✅	4s	2s	+100%
`sign_signature_pre_hash_internal`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	3s	+33%
`intt_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_avx2`	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	✅	3s	3s	+0%
`keccakf1600_permute`	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	3s	+0%
`montgomery_reduce`	✅	3s	3s	+0%
`ntt_native_aarch64`	✅	3s	6s	-50%
`nttunpack_native_x86_64`	✅	3s	3s	+0%
`pack_sig_c`	✅	3s	4s	-25%
`pack_sig_h`	✅	3s	4s	-25%
`pack_sk_s1`	✅	3s	1s	+200%
`pointwise_acc_native_x86_64`	✅	3s	6s	-50%
`poly_add`	✅	3s	6s	-50%
`poly_caddq_c`	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	✅	3s	2s	+50%
`poly_challenge`	✅	3s	5s	-40%
`poly_chknorm_native_aarch64`	✅	3s	4s	-25%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	✅	3s	5s	-40%
`poly_decompose_native_x86_64`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	5s	-40%
`poly_power2round`	✅	3s	3s	+0%
`poly_uniform_gamma1`	✅	3s	4s	-25%
`poly_use_hint`	✅	3s	1s	+200%
`poly_use_hint_native`	✅	3s	3s	+0%
`polyt1_unpack`	✅	3s	4s	-25%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	3s	+0%
`polyveck_pack_w1`	✅	3s	3s	+0%
`polyveck_reduce`	✅	3s	3s	+0%
`polyvecl_chknorm`	✅	3s	7s	-57%
`polyvecl_uniform_gamma1`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	✅	3s	4s	-25%
`polyz_pack`	✅	3s	5s	-40%
`polyz_unpack_native_x86_64`	✅	3s	3s	+0%
`rej_eta`	✅	3s	4s	-25%
`rej_uniform_native`	✅	3s	8s	-62%
`shake128_absorb`	✅	3s	4s	-25%
`shake128x4_absorb_once`	✅	3s	5s	-40%
`sign_signature`	✅	3s	5s	-40%
`sign_signature_extmu`	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	✅	3s	6s	-50%
`sign_verify`	✅	3s	5s	-40%
`sign_verify_extmu`	✅	3s	3s	+0%
`sign_verify_pre_hash_internal`	✅	3s	3s	+0%
`sk_s2hat_get_poly`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	4s	-25%
`decompose`	✅	2s	3s	-33%
`fqscale`	✅	2s	3s	-33%
`intt_native_x86_64`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	4s	-50%
`keccak_finalize`	✅	2s	1s	+100%
`keccak_squeeze`	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes`	✅	2s	3s	-33%
`make_hint`	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	✅	2s	4s	-50%
`mld_ct_get_optblocker_i64`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mld_h`	✅	2s	3s	-33%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	4s	-50%
`mld_prepare_domain_separation_prefix`	✅	2s	4s	-50%
`mld_value_barrier_i64`	✅	2s	1s	+100%
`mld_value_barrier_u32`	✅	2s	2s	+0%
`ntt_native_x86_64`	✅	2s	2s	+0%
`pack_sig_z`	✅	2s	5s	-60%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native`	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_native`	✅	2s	2s	+0%
`poly_invntt_tomont`	✅	2s	1s	+100%
`poly_ntt`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	4s	-50%
`poly_shiftl`	✅	2s	4s	-50%
`poly_sub`	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	✅	2s	3s	-33%
`poly_use_hint_c`	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	4s	-50%
`polyt0_pack`	✅	2s	4s	-50%
`polyveck_pack_eta`	✅	2s	6s	-67%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	5s	-60%
`polyz_unpack`	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	✅	2s	4s	-50%
`power2round`	✅	2s	4s	-50%
`reduce32`	✅	2s	3s	-33%
`rej_eta_c`	✅	2s	5s	-60%
`rej_eta_native`	✅	2s	6s	-67%
`rej_uniform_eta_native_aarch64`	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`shake128_release`	✅	2s	4s	-50%
`shake128x4_squeezeblocks`	✅	2s	3s	-33%
`shake256_absorb`	✅	2s	2s	+0%
`shake256_release`	✅	2s	3s	-33%
`shake256x4_absorb_once`	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	✅	2s	1s	+100%
`sk_s1hat_get_poly`	✅	2s	3s	-33%
`sys_check_capability`	✅	2s	3s	-33%
`unpack_pk_t1`	✅	2s	1s	+100%
`unpack_sk`	✅	2s	5s	-60%
`unpack_sk_t0hat`	✅	2s	7s	-71%
`caddq`	✅	1s	4s	-75%
`keccak_f1600_x1_native_aarch64`	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	4s	-75%
`keccak_init`	✅	1s	3s	-67%
`keccakf1600_permute_native`	✅	1s	4s	-75%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_ct_abs_i32`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	✅	1s	3s	-67%
`mld_ct_sel_int32`	✅	1s	3s	-67%
`mld_keccakf1600_extract_bytes`	✅	1s	4s	-75%
`mld_sign_finish`	✅	1s	-	new
`mld_sign_resume`	✅	1s	-	new
`mld_value_barrier_u8`	✅	1s	3s	-67%
`pack_sk_rho_key_tr_s2`	✅	1s	3s	-67%
`pointwise_native_x86_64`	✅	1s	2s	-50%
`poly_caddq_native`	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	✅	1s	3s	-67%
`poly_invntt_tomont_native`	✅	1s	5s	-80%
`poly_permute_bitrev_to_custom_optional`	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	5s	-80%
`poly_reduce`	✅	1s	2s	-50%
`poly_uniform`	✅	1s	4s	-75%
`poly_uniform_eta`	✅	1s	4s	-75%
`polyveck_unpack_eta`	✅	1s	4s	-75%
`polyvecl_unpack_eta`	✅	1s	5s	-80%
`polyw1_pack`	✅	1s	4s	-75%
`polyw1_pack_32`	✅	1s	4s	-75%
`polyw1_pack_88`	✅	1s	3s	-67%
`polyz_unpack_native`	✅	1s	4s	-75%
`rej_uniform_native_aarch64`	✅	1s	2s	-50%
`shake128_finalize`	✅	1s	2s	-50%
`shake128_init`	✅	1s	1s	+0%
`shake128_squeeze`	✅	1s	2s	-50%
`shake256`	✅	1s	2s	-50%
`shake256_finalize`	✅	1s	2s	-50%
`shake256_init`	✅	1s	2s	-50%
`unpack_sk_s1hat`	✅	1s	2s	-50%
`use_hint`	✅	1s	3s	-67%
`yvec_get_poly`	✅	1s	4s	-75%
`yvec_init`	✅	1s	4s	-75%

hanno-becker · 2026-08-26T04:54:56Z

+ * Set this only to change the alignment. Wherever mldsa-native knows a
+ * declarator prefix for the compiler, that prefix follows the new value
+ * automatically; otherwise set MLD_CONFIG_ALIGN_ATTRIBUTE as well.


It's not clear to me what "herever mldsa-native knows a declarator prefix for the compiler, that prefix follows the new value automatically" means. Can you rephrase?

hanno-becker · 2026-08-26T04:55:28Z

+ * alignment-sensitive load and store instructions; this is enforced at
+ * compile time.


It should be clarified if this means a silent alignment bump or a rejection.

hanno-becker · 2026-08-26T04:56:54Z

+ *
+ * Declarator prefix aligning the declared object.
+ *
+ * Set this only if mldsa-native knows no spelling for your compiler. Without


It's unclear what "Set this only if mldsa-native knows no spelling for your compiler." means.

hanno-becker · 2026-08-26T05:00:37Z

+#define MLD_DEFAULT_ALIGN MLD_CONFIG_ALIGN
+#else
 #define MLD_DEFAULT_ALIGN 32


MLD_DEFAULT_ALIGN is perhaps no longer the right name?

hanno-becker · 2026-08-26T05:02:07Z

+/* This backend loads and stores polynomials through Q registers, which fault
+ * on operands that are not 16-byte aligned if alignment checking is on. */
+#if MLD_DEFAULT_ALIGN < 16
+#error Bad configuration: The AArch64 backend requires MLD_CONFIG_ALIGN to be at least 16


Perhaps say why

hanno-becker · 2026-08-26T05:02:17Z

+/* This backend loads and stores polynomials with vmovdqa, which faults on
+ * operands that are not 32-byte aligned. */
+#if MLD_DEFAULT_ALIGN < 32
+#error Bad configuration: The x86_64 backend requires MLD_CONFIG_ALIGN to be at least 32


Perhaps say why here, too

hanno-becker · 2026-08-26T05:03:40Z


+/* This backend loads and stores polynomials through Q registers, which fault
+ * on operands that are not 16-byte aligned if alignment checking is on. */
+#if MLD_DEFAULT_ALIGN < 16


We should also catch the case where we don't know an alignment declarator. In that case, one should arguably refuse to build the backends. One way to do this would be to check first if an alignment declarator is known, and if not, set the alignment to 1.

hanno-becker

Overall this looks good, thanks @mkannwischer! Some documentation nits in comments. We should also use this opportunity to fix the pre-existing defect that if no alignment declarator is known, we silently build the backends without alignment constraints.

mkannwischer force-pushed the configurable-alignment branch from 8c86285 to b64cbd8 Compare August 11, 2026 05:37

mkannwischer marked this pull request as ready for review August 11, 2026 06:37

mkannwischer requested a review from a team as a code owner August 11, 2026 06:37

hanno-becker reviewed Aug 26, 2026

View reviewed changes

hanno-becker requested changes Aug 26, 2026

View reviewed changes

		* alignment-sensitive load and store instructions; this is enforced at
		* compile time.

Uh oh!

Conversation

mkannwischer commented Aug 11, 2026

Uh oh!

oqs-bot commented Aug 11, 2026

CBMC Results (ML-DSA-65, REDUCE-RAM)

Uh oh!

oqs-bot commented Aug 11, 2026

CBMC Results (ML-DSA-44, REDUCE-RAM)

Uh oh!

oqs-bot commented Aug 11, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Aug 11, 2026

CBMC Results (ML-DSA-87, REDUCE-RAM)

Uh oh!

oqs-bot commented Aug 11, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Aug 11, 2026

CBMC Results (ML-DSA-87)

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hanno-becker left a comment •

edited

Loading